/*
Copyright 2013 Nicola Olivetti, Gian Luca Pozzato. This file is part of NESCOND.NESCOND is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version. NESCOND is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with NESCOND. If not, see <http://www.gnu.org/licenses/>.
*/

/* imports */
:- use_module(library(lists)).
:- use_module(operators).
:- use_module(library(timeout)).

/* 
['/Users/gpozzato/Desktop/nested sequents/implementazione/ckidcem.pl'].
*/

/* A nested sequent Gamma is a Prolog list of the form:

   Gamma = [F_1, F_2, ..., F_m, [[A_1,Gamma_1],AppliedConditionals_1], [[A_2,Gamma_2],AppliedConditionals_2], ..., [[A_n,Gamma_n],AppliedConditionals_n]]  ]

   where F_i are formulas of the conditional language, A_i are formulas of the conditional language and Gamma_i are Prolog lists representing nested sequents.

  --------------------------------------------------------------------------------------------------------------------------------------------------------------

   A context is a pair [Context,AppliedConditionals] where:
   - Context has the form [Fml,Gamma], where Fml is a formula of the conditional language and Gamma is a Prolog list representing a nested sequent
   - AppliedConditionals is a Prolog list [A_1=>B_1,A_2=>B_2,...,A_k=>B_k]
   such that the rule (=>-) has been already applied to each formula in AppliedConditionals by using Context.
   
   Example: [[A,Gamma],[B=>C,D=>E]] means that (=>-) has been already applied to B=>C and D=>E with [A:Gamma] in the current branch.

   This list is used in order to ensure the termination of the calculi.

*/


fillTheHole(NS,ListToFill,NewNS):-select(hole,NS,TempNS),!,
								  append(TempNS,ListToFill,NewNS).
fillTheHole(NS,ListToFill,[[[Fml,NewGamma],AppliedConditionals,AllowID]|TempNS]):-select([[Fml,Gamma],AppliedConditionals,AllowID],NS,TempNS),
								  fillTheHole(Gamma,ListToFill,NewGamma).

selectList([],NS,[hole|NS]).
selectList([Fml|Tail],NS,NewNS):-select(Fml,NS,TempNS),
								 selectList(Tail,TempNS,NewNS).
						
deepSelect(List,NS,NewNS):-selectList(List,NS,NewNS).
deepSelect(List,NS,[[[Fml,NewGamma],AppliedConditionals,AllowID]|NewNS]):-select([[Fml,Gamma],AppliedConditionals,AllowID],NS,NewNS),
						   deepSelect(List,Gamma,NewGamma).

memberList([],_).
memberList([Head|Tail],NS):-member(Head,NS),memberList(Tail,NS).
deepMember(List,NS):-memberList(List,NS).
deepMember(List,NS):-member([[_,Gamma],_,_],NS),
					 deepMember(List,Gamma).

/* Partition a nested sequent A_1, A_2, ..., A_n, [[B_1,Gamma_1],Appl1], [[B_2,Gamma_2],Appl2], ..., [[B_m,Gamma_m],Applm]
  into formulas and contexts */
partitionNS([],[],[]):-!.
partitionNS([[[B,Gamma],AppliedConditional,AllowID]|Tail],Formulas,[[[B,Gamma],AppliedConditional,AllowID]|Contexts]):-!,
  partitionNS(Tail,Formulas,Contexts).
partitionNS([F|Tail],[F|Formulas],Contexts):-!,partitionNS(Tail,Formulas,Contexts).

/* Extract subcontexts from a nested sequent */
extractSubContexts([],[]):-!.
extractSubContexts([[[_,Delta],_,_]|Tail],[Delta|ResTail]):-!,extractSubContexts(Tail,ResTail).
extractSubContexts([_|Tail],ResTail):-extractSubContexts(Tail,ResTail).
/* List all contexts [A,Gamma] for a given A */
listAllContexts(_,[],[]):-!.
listAllContexts(A,[[A,Gamma]|Tail],[Gamma|ResTail]):-!,listAllContexts(A,Tail,ResTail).
listAllContexts(A,[_|Tail],ResTail):-!,listAllContexts(A,Tail,ResTail).

notSequentIncluded(Delta,Sigma):-
  partitionNS(Delta,Formulas,Contexts),!,
  ((member(F,Formulas),\+member(F,Sigma),!)
   ;
  (extractSubContexts(Sigma,List),member([[A,Gamma],_],Contexts),notSeqList(A,Gamma,List))).
notSeqList(_,_,[]):-!.
notSeqList(A,_,List):-true,\+member([A,_],List),!.
notSeqList(A,Gamma,List):-listAllContexts(A,List,Delta),recNotSeqList(Gamma,Delta).
recNotSeqList(_,[]):-!.
recNotSeqList(Gamma,[Delta|Tail]):-notSequentIncluded(Gamma,Delta),recNotSeqList(Gamma,Tail).

/* Axioms closing branches */
prove(NS,tree(ax)):-deepMember([P,!P],NS),!.
prove(NS,tree(axt)):-deepMember([top],NS),!.
prove(NS,tree(axb)):-deepMember([!bot],NS),!.
/* Rules with one premise */
prove(NS,tree(neg,A,SubTree)):-deepSelect([!!A],NS,NewNS),!,fillTheHole(NewNS,[A],DefNS),prove(DefNS,SubTree).
prove(NS,tree(orp,A,B,SubTree)):-deepSelect([A v B],NS,NewNS),!,fillTheHole(NewNS,[A,B],DefNS),prove(DefNS,SubTree).
prove(NS,tree(andn,A,B,SubTree)):-deepSelect([!(A ^ B)],NS,NewNS),!,fillTheHole(NewNS,[!A,!B],DefNS),prove(DefNS,SubTree).
prove(NS,tree(impp,A,B,SubTree)):-deepSelect([A -> B],NS,NewNS),!,fillTheHole(NewNS,[!A,B],DefNS),prove(DefNS,SubTree).
prove(NS,tree(condp,A,B,SubTree)):-deepSelect([A => B],NS,NewNS),!,fillTheHole(NewNS,[[[A,[B]],[],true]],DefNS),prove(DefNS,SubTree).
/* Rules with two or three premises (introducing a branch in a backward proof search) */
prove(NS,tree(orn,A,B,Sub1,Sub2)):-deepSelect([!(A v B)],NS,NewNS),!,fillTheHole(NewNS,[!A],NS1),fillTheHole(NewNS,[!B],NS2),prove(NS1,Sub1),prove(NS2,Sub2).
prove(NS,tree(andp,A,B,Sub1,Sub2)):-deepSelect([A ^ B],NS,NewNS),!,fillTheHole(NewNS,[A],NS1),fillTheHole(NewNS,[B],NS2),prove(NS1,Sub1),prove(NS2,Sub2).
prove(NS,tree(impn,A,B,Sub1,Sub2)):-deepSelect([!(A -> B)],NS,NewNS),!,fillTheHole(NewNS,[A],NS1),fillTheHole(NewNS,[!B],NS2),prove(NS1,Sub1),prove(NS2,Sub2).
prove(NS,tree(id,A,SubTree)):-deepSelect([[[A,Delta],AppliedConditionals,true]],NS,NewNS),!,
      fillTheHole(NewNS,[[[A,[!A|Delta]],AppliedConditionals,false]],DefNS),prove(DefNS,SubTree).
prove(NS,tree(condn,A,B,Sub1,Sub2,Sub3)):-
    deepSelect([!(A => B),[[C,Delta],AppliedConditionals,AllowID]],NS,NewNS),
    \+member(!(A => B),AppliedConditionals),
    prove([A,!C],Sub2),
    prove([C,!A],Sub3),!,
    fillTheHole(NewNS,[!(A => B),[[C,[!B|Delta]],[!(A => B)|AppliedConditionals],AllowID]],DefNS),
    prove(DefNS,Sub1).
/* In order to obtain a terminating calculus, the clause implementing the rule (CEM) is the last one of the program.
   This corresponds to apply (CEM) to CEM-reduced sequents, that is to say sequents in which we have already applied 
  (=>-) as much as possible to each negated conditional !(C=>D). Furthermore,  CEM-reduced sequents contain only atomic 
  formulas and negated conditionals, therefore all subformulas of !D have been introduced in the involved contexts. */
prove(NS,tree(cem,A,B,Sub1,Sub2,Sub3)):-
    deepSelect([[[A,Delta],ApplCond1,AllowID1],[[B,Sigma],ApplCond2,AllowID2]],NS,NewNS),
    notSequentIncluded(Delta,Sigma),
    prove([A,!B],Sub2),
    prove([B,!A],Sub3),
    append(Delta,Sigma,ResDelta),
    fillTheHole(NewNS,[[[A,ResDelta],ApplCond1,AllowID1],[[B,Sigma],ApplCond2,AllowID2]],DefNS),
    prove(DefNS,Sub1).


test(Fml,Msec,Result):-time_out(prove([Fml],_),Msec,Result).